home *** CD-ROM | disk | FTP | other *** search
/ Belgian Amiga Club - ADF Collection / BS1 part 34.zip / BS1 part 34 / FredFish PD 316.adf / Formulae / ReadMe < prev    next >
Text File  |  1990-02-06  |  4KB  |  101 lines
  1.  
  2.                                       Formulae
  3.                              by Gauthier Groult, May 89
  4.  
  5.  
  6.           This  code  is  part  of  an  academic project I worked on at the
  7.           University  of  Sciences  of  Paris   7,   Jussieu.   It   is  an
  8.           implementation  of   basic  propositional  formulae  manipulation
  9.           routines in Scheme. An excellent version of Scheme  was ported to
  10.           the Amiga  by Ed  Puckett (MIT  Branch) and  can be found on Fish
  11.           disk #149. Thank you for that, Ed!
  12.  
  13.           The source file is commented... in french. So  here are  the high
  14.           level functions and what they do:
  15.  
  16.                empty
  17.                     returns the empty set
  18.  
  19.                singleton(x)
  20.                     returns a one element set containing x
  21.  
  22.                add(elem, set)
  23.                     adds the element elem to the set set
  24.  
  25.                union(set1, set2)
  26.                     returns the union of sets set1 and set2
  27.  
  28.                inter(set1, set2)
  29.                     returns the intersection of the two sets
  30.  
  31.                product(set1, set2) 
  32.                     returns  the  cartesian  (Descartes  was french, by the
  33.                     way) product of set1 and set2
  34.  
  35.                axioms
  36.                     returns a list of  the 14  axioms of  the propositional
  37.                     calculus.  These  are  arbitrary  axioms, they could be
  38.                     replaced by equivalents.
  39.  
  40.                formula?(f)
  41.                     tests if f is a propositional  formula. See  at the end
  42.                     of this list the conventions used to write formulae.
  43.  
  44.                vars?(f)
  45.                     Returns a list of the variables contained in f, where f
  46.                     is supposed to be a formula.
  47.  
  48.                subst(f, v, g)
  49.                     replaces each occurrence of the variable v in  f by the
  50.                     formula g, where f is supposed to be a formula.
  51.  
  52.                table(varset)
  53.                     returns  the   set  of  all  possible  assignations  of
  54.                     variables in varset to true or false.
  55.  
  56.                true?(f, a)
  57.                     returns the value of f under a, where f is  supposed to
  58.                     be  a   correct  formula   and  a  correct  assignation
  59.                     (conventions below).
  60.  
  61.                valid?(f)
  62.                     decides whether  f is  a valid  formula, i.e.  if it is
  63.                     always true.
  64.                refute(f)
  65.                     returns  a  list  of  all  the  assignations refuting f
  66.                     (giving the value false to f), f being a formula.
  67.  
  68.                sheffer?(f)
  69.                     tests if f satisfies the Sheffer theorem, where  f is a
  70.                     formula.
  71.  
  72.                shefferize(stroke, name, f)
  73.                     translates any formula f into a formula built only with
  74.                     the new connector  name,  which  itself  represents the
  75.                     Sheffer formula stroke.
  76.  
  77.           Formulae  are  written  as  postfixed  lists  -  reversed  polish
  78.           notation. The connectors  are  named  "not",  "et",  "ou", "imp",
  79.           "equiv" for  negation, and,  or, implication and equivalency. The
  80.           names can be easily changed to anything else.
  81.  
  82.           The formula
  83.                               "not a implicates (b and c)" 
  84.           then becomes
  85.                               (imp (non a) (et b c))
  86.           with these rules.
  87.  
  88.           Assignations are sets (lists)  of two  elements, where  the first
  89.           element is  the variable  and the  second its value: (a #t) is an
  90.           assignation representing the  variable  a  with  the  value true.
  91.           Values can be #t or #f.
  92.  
  93.  
  94.           Sheffer formulae  or basically  NANDs and  NORs. You  can try for
  95.           instance "(shefferize '(non (et (a b))) '+ '(ou a b))".
  96.  
  97.  
  98.           I hope this will be helpful to someone.
  99.  
  100.  
  101.